$\forall$$T$:Type, $P$:($T$$\rightarrow$Prop).
\\[0ex]AtomFree(Type;$T$) $\Rightarrow$ AtomFree($T$$\rightarrow$Prop;$P$) $\Rightarrow$ AtomFree(Type;\{$t$:$T$$\mid$ $P$($t$) \})